package dpll.fnc;

import dpll.ast.IASTNode;
import dpll.ast.NodoBiCondicion;
import dpll.ast.NodoBooleano;
import dpll.ast.NodoCondicion;
import dpll.ast.NodoConjuncion;
import dpll.ast.NodoDisyuncion;
import dpll.ast.NodoFormula;
import dpll.ast.NodoFormulas;
import dpll.ast.NodoLiteral;
import dpll.ast.NodoNegacion;
import dpll.ast.NodoParentesis;
import dpll.ast.NodoTerminoFinal;

public class FNCVisitor implements IVisitor<IASTNode> {
	
	private boolean cambio = false;

	@Override
	public IASTNode visit(IASTNode node) {
		return node.accept(this);
	}

	@Override
	public IASTNode visitFormula(NodoFormula node) {
		return new NodoFormula(visit(node.getProposicion()));
	}

	@Override
	public IASTNode visitFormulas(NodoFormulas node) {
		NodoFormulas formulas = new NodoFormulas();
		for (IASTNode formula: node.getFormulas())
			formulas.addFormula(visit(formula));
		return formulas;
			
	}

	@Override
	public IASTNode visitParentesis(NodoParentesis node) {
		return visit(node.getProposicion());
	}

	@Override
	public IASTNode visitNegacion(NodoNegacion node) {
		//doble negacion - para interiorizar la negacion
		if (node.getProposicion() instanceof NodoNegacion) {
			cambio = true;
			return visit(((NodoNegacion) node.getProposicion()).getProposicion());
		}
		//morgan operador Y - para interiorizar la negacion
		else if (node.getProposicion() instanceof NodoConjuncion) {
			cambio = true;
			return new NodoDisyuncion(new NodoNegacion(visit(((NodoConjuncion) node.getProposicion()).GetIz())), new NodoNegacion(visit(((NodoConjuncion) node.getProposicion()).GetDc())));
		}
		//morgan operador O - para interiorizar la negacion
		else if (node.getProposicion() instanceof NodoDisyuncion) {
			cambio = true;
			return new NodoConjuncion(new NodoNegacion(visit(((NodoDisyuncion) node.getProposicion()).GetIz())), new NodoNegacion(visit(((NodoDisyuncion) node.getProposicion()).GetDc())));
		}
		else if (node.getProposicion() instanceof NodoBooleano) {
			cambio = true;
			//valor TRUE negado
			if (((NodoBooleano) node.getProposicion()).getValor())
				return new NodoBooleano("FALSE");
			//valor FALSE negado
			else
				return new NodoBooleano("TRUE");
		}
		else
			return new NodoNegacion(visit(node.getProposicion()));
	}

	@Override
	public IASTNode visitConjuncion(NodoConjuncion node) {
		if (node.GetIz() instanceof NodoBooleano) {
			cambio = true;
			//valor TRUE en conjuncion por la izquierda
			if (((NodoBooleano) node.GetIz()).getValor())
				return visit(node.GetDc());
			//valor FALSE en conjuncion por la izquierda
			else
				return new NodoBooleano("FALSE");
		}
		else if (node.GetDc() instanceof NodoBooleano) {
			cambio = true;
			//valor TRUE en conjuncion por la derecha
			if (((NodoBooleano) node.GetDc()).getValor())
				return visit(node.GetIz());
			//valor FALSE en conjuncion por la derecha
			else
				return new NodoBooleano("FALSE");
		}
		else
			return new NodoConjuncion(visit(node.GetIz()), visit(node.GetDc()));
	}

	@Override
	public IASTNode visitDisyuncion(NodoDisyuncion node) {
		//distributividad operador O por la derecha - interiorizar operador O, exteriorizar operador Y
		if (node.GetDc() instanceof NodoConjuncion) {
			cambio = true;
			return new NodoConjuncion(new NodoDisyuncion(visit(node.GetIz()), visit(((NodoConjuncion) node.GetDc()).GetIz())), new NodoDisyuncion(visit(node.GetIz()), visit(((NodoConjuncion) node.GetDc()).GetDc())));
		//distributividad operador O por la izquierda - interiorizar operador O, exteriorizar operador Y
		}
		else if (node.GetIz() instanceof NodoConjuncion) {
			cambio = true;
			return new NodoConjuncion(new NodoDisyuncion(visit(((NodoConjuncion) node.GetIz()).GetIz()), visit(node.GetDc())), new NodoDisyuncion(visit(((NodoConjuncion) node.GetIz()).GetDc()), visit(node.GetDc())));
		}
		else if (node.GetIz() instanceof NodoBooleano) {
			cambio = true;
			//valor TRUE en disyuncion por la izquierda
			if (((NodoBooleano) node.GetIz()).getValor())
				return new NodoBooleano("TRUE");
			//valor FALSE en disyuncion por la izquierda
			else
				return visit(node.GetDc());
		}
		else if (node.GetDc() instanceof NodoBooleano) {
			cambio = true;
			//valor TRUE en disyuncion por la derecha
			if (((NodoBooleano) node.GetDc()).getValor())
				return new NodoBooleano("TRUE");
			//valor FALSE en disyuncion por la derecha
			else
				return visit(node.GetIz());
		}
		else 
			return new NodoDisyuncion(visit(node.GetIz()), visit(node.GetDc()));
	}

	@Override
	public IASTNode visitCondicion(NodoCondicion node) {
		//eliminacion operador SI
		cambio = true;
		return new NodoDisyuncion(new NodoNegacion(visit(node.GetIz())), visit(node.GetDc()));
	}

	@Override
	public IASTNode visitBiCondicion(NodoBiCondicion node) {
		//eliminacion operador SISOLOSI
		cambio = true;
		return new NodoConjuncion(new NodoDisyuncion(new NodoNegacion(visit(node.GetIz())), visit(node.GetDc())), new NodoDisyuncion(new NodoNegacion(visit(node.GetDc())), visit(node.GetIz())));
	}

	@Override
	public IASTNode visitTerminoFinal(NodoTerminoFinal node) {
		return visit(node.getTermino());
	}

	@Override
	public IASTNode visitBooleano(NodoBooleano node) {
		return node;
	}

	@Override
	public IASTNode visitLiteral(NodoLiteral node) {
		return node;
	}

	public boolean isCambio() {
		return cambio;
	}

	public void setCambio(boolean cambio) {
		this.cambio = cambio;
	}

}
